Nuprl Lemma : ecl-trans-act_wf
0,22
postcript
pdf
ds
:
x
:Id fp
Type,
da
:
k
:Knd fp
Type,
A
:ecl-trans-tuple{i:l}(
ds
;
da
).
ecl-trans-act(
ds
;
da
;
A
)
(event-info(
ds
;
da
) List)
Prop
latex
Definitions
t
T
,
Valtype(
da
;
k
)
,
P
Q
,
False
,
A
,
A
B
,
,
x
:
A
.
B
(
x
)
,
ecl-trans-state(
v
;
L
)
,
ecl-trans-ks(
v
)
,
Knd
,
(
x
l
)
,
ecl-trans-a(
v
)
,
b
,
Prop
,
A
&
B
,
event-info(
ds
;
da
)
,
let
x
,
y
,
z
=
a
in
t
(
x
;
y
;
z
)
,
as
@
bs
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
ecl-trans-act(
ds
;
da
;
A
)
,
Id
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
ecl-trans-tuple{i:l}(
ds
;
da
)
Lemmas
ecl-trans-tuple
wf
,
fpf
wf
,
Id
wf
,
append
wf
,
event-info
wf
,
nat
wf
,
assert
wf
,
ecl-trans-a
wf
,
l
member
wf
,
Knd
wf
,
ecl-trans-ks
wf
,
ecl-trans-state
wf
origin
ds:x:Id fp
Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da).
(event-info(ds;da) List)Prop ds:x:Id fp Type, da:k:Knd fp Type, A:ecl-trans-tuple{i:l}(ds;da).
(event-info(ds;da) List)Prop 
Q
A
B
b
x:A. B(x)
x. t(x)